(declare-fun _substvar_777_ () Bool)
(declare-fun _substvar_793_ () Bool)
(declare-fun _substvar_936_ () Bool)
(declare-fun _substvar_845_ () Bool)
(declare-fun _substvar_848_ () Bool)
(declare-const r0 Real)
(declare-const r1 Real)
(declare-const r5 Real)
(push)
(declare-const v6 Bool)
(declare-const v16 Bool)
(assert (or v6 (<= 94.41153 (* (+ r5 r1 r0 69718878.0) 69718878.0 r5 r0)) _substvar_936_))
(assert _substvar_845_)
(assert _substvar_848_)
(assert (or v6 (distinct 69718878.0 (- r5 69718878.0 r0) 0.0)))
(assert _substvar_777_)
(assert (or v16 _substvar_793_ v6))
(check-sat)
